Nuprl Lemma : map_select
11,40
postcript
pdf
A
,
B
:Type,
f
:(
A
B
),
as
:(
A
List),
n
:int_seg(0; ||
as
||). map(
f
;
as
)[
n
] =
f
(
as
[
n
])
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Y
,
map(
f
;
as
)
,
||
as
||
,
P
Q
,
P
Q
,
P
Q
,
P
Q
,
False
,
A
,
A
B
,
lelt(
i
;
j
;
k
)
,
int_seg(
i
;
j
)
,
P
Q
,
decidable(
P
)
Lemmas
length
wf1
,
int
seg
wf
,
decidable
int
equal
,
select
cons
hd
,
map
wf
,
select
cons
tl
,
map
length
,
non
neg
length
origin
A,B:Type, f:(A
B), as:(A List), n:int_seg(0; ||as||). map(f; as)[n] = f(as[n]) A,B:Type, f:(AB), as:(A List), n:int_seg(0; ||as||). map(f; as)[n] = f(as[n]) 
Tx:A. B(x)
Q
Q
Q Q
A
B
Q